FDL - Nuprl Lemma : single-threaded-relation3

Nuprl Lemma : single-threaded-relation3

es:ES, P:(E

), R:(E

E

).
(

e:E. Dec(P(e)))

(

e, e':E. Dec(R(e',e)))

R =>

x,y. (x < y)

(

e, e':E. (P(e) & R(e',e))

P(e'))

(

m, m':E.

P(m)

P(m')

(

e:E. (e R m)

(

P(e)))

(

e:E. (e R m')

(

P(e)))

(m = m'))

(

a, b, e:E.

(

x, y:E. x c

e

y c

e

P(x)

P(y)

(((x R^+ y)

(x = y))

(y R^+ x)))

(R(e,a) & R(e,b))

(P(e) & P(a) & P(b))

(

z:E.

(R^+(e,z) & R^+(z,a) & P(z)))

(

z:E.

(R^+(e,z) & R^+(z,b) & P(z)))

(a = b))

(

e, e':E. P(e)

P(e')

(((e R^+ e')

(e = e'))

(e' R^+ e)))

Definitions Trans(T;x,y.E(x;y)), t T, P Q, x f y, P & Q, x(s), P Q, , x:A. B(x), False, A, x:A. B(x), R1 => R2

Lemmas rel plus trans, single-threaded-relation, rel-rel-plus, rel plus implies, es-causl transitivity, rel plus minimal, decidable rel plus-causl, event system wf, decidable wf, es-causl wf, rel implies wf, not wf, rel plus wf, es-causle wf, es-E wf